Polynomial Generators have MCA for RSCodes by katyhr · Pull Request #610 · Verified-zkEVM/ArkLib

katyhr · 2026-07-06T17:59:42Z

This PR formalises

MCA error function for MDS codes (appears in the statement of Theorem 6.1 [BCGM25]).
Statement of Theorem 6.1 (MCA for MDS generators) [BCGM25].
Definition 8.1 (MCA error for univariate powers) [BCGM25].
Theorem 8.2 (polynomial_gen_MCA) [BCGM25] (statement and proof).
Definition 9.1 [BCGM25].
Statement of Lemma 9.3 (univariate_powers_MCA) [BCGM25].
Theorem 9.2 (polynomial_gen_MCA_RScode) [BCGM25] (statement and proof assuming Lemma 9.3).

Interesting outcomes:

We prove an s-fold tensor product lemma tensor_of_univ_is_MCA that is assumed in the proof of Theorem 9.2. In fact, we prove a more general version of this result. In the paper, the result is stated only for a Reed-Solomon code. We prove this for a univariate generator of any code!
Additionally, we explicitly contract the matrix A that appears in the proof of Theorem 9.2.

github-actions · 2026-07-06T18:00:06Z

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Polynomial Generators have MCA for RSCodes

sorry delta: +3 (3 added) — proof obligations increased

The PR formalizes the MCA property for polynomial generators over Reed–Solomon codes, primarily proving Theorem 9.2 of [BCGM25] conditionally on two sorried lemmas. It also reorganizes the proximity generator module hierarchy and adds several supporting definitions and lemmas.

Statistics

Metric	Count
📝 Files Changed	12
✅ Lines Added	1089
❌ Lines Removed	171

Lean Declarations

✏️ Removed: 7 declaration(s)

ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean (7)

def generatorByRightMul (G : Generator S ℓ F) (A : Matrix ℓ ℓ' F) : Generator S ℓ' F
def matrixMulCodewords (A : Matrix ℓ ℓ' F) (U : ℓ' → (ι → F)) : ℓ → (ι → F)
def projectedGenerator (G : Generator S ℓ F) (κ : Set ℓ) : Generator S κ F
lemma generatorSubset [Nonempty S] (G : Generator S ℓ F) (ε_mca : I → I) (LC : LinearCode ι F)
lemma isMCA_projectedGenerator_of_isMCA (LC : LinearCode ι F) [Nonempty S] (G : Generator S ℓ F)
lemma pseudoinverseGen [DecidableEq ℓ'] [Nonempty S] (G : Generator S ℓ F) (ε_mca : I → I)
noncomputable def zeroExtend (κ : Set ℓ) (U : κ → (ι → F)) : ℓ → (ι → F)

✏️ Added: 46 declaration(s)

ArkLib/Data/CodingTheory/Basic/LinearCode.lean (1)

def projectedCode_submod

ArkLib/Data/CodingTheory/Prelims.lean (3)

abbrev affineComb {s : ℕ} (U : Fin (s + 1) → (ι → F)) (x : Fin s → F) : ι → F
abbrev linComb {s : ℕ} (U : Fin (s + 1) → (ι → F)) (l : Fin s → F) : ι → F
lemma affineComb_line {s : ℕ} (U : Fin (s + 1) → (ι → F)) (v lam : Fin s → F) (t : F) :

ArkLib/Data/CodingTheory/ProximityGenerator/AffineGenerator.lean (8)

abbrev projectedQuotient [Fintype ι] (LC : LinearCode ι F) (T : Finset ι) : Type
lemma exists_avg_le [Fintype F] {s : ℕ} (hs : 1 ≤ s) (f : (Fin s → F) → ℕ) (m : ℕ)
lemma exists_dir_line_ge [Fintype F] [Nonempty F] {s : ℕ}
lemma exists_line_bound [Fintype F] [Fintype ι] {s : ℕ} (hs : 1 ≤ s)
lemma exists_succ_not_mem [Fintype ι] {s : ℕ} (LC : LinearCode ι F) (T : Finset ι)
lemma line_vecMul (W : Fin 2 → (ι → F)) (t : F) :
lemma proj_lincomb_ker_card_le [Fintype F] [Fintype ι] {s : ℕ}
theorem AffineLine_MCA_AffineSpaceMCA {ℓ : ℕ} (hℓ : ℓ ≥ 2) (ε_mca : I → ℝ) (LC : LinearCode ι F)

ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean (5)

abbrev AffineLineGenerator (F : Type) [Field F] : Generator F (Fin 2) F
abbrev AffineSpaceGenerator (F : Type) [Field F] (ℓ : ℕ) : Generator (Fin ℓ → F) (Fin (ℓ + 1)) F
def IsPolynomialGeneratorOfFull {s : ℕ} (G : Generator (Fin s → F) ℓ F)
def UnivariatePowers (d : ℕ) : Generator F (Fin (d + 1)) F
lemma vecMul_tensorGenerator_explicit {ℓ' : Type} [Fintype ℓ'] {S S' : Type}

ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean (10)

def generatorByRightMul (G : Generator S ℓ F) (A : Matrix ℓ ℓ' F) : Generator S ℓ' F
def matrixMulCodewords (A : Matrix ℓ ℓ' F) (U : ℓ' → (ι → F)) : ℓ → (ι → F)
def projectedGenerator (G : Generator S ℓ F) (κ : Set ℓ) : Generator S κ F
lemma generatorSubset [Nonempty S] (G : Generator S ℓ F) (ε_mca : I → ℝ) (LC : LinearCode ι F)
lemma isMCAGenerator_reindex {S' : Type} [Fintype S'] [Nonempty S'] [Nonempty S]
lemma isMCA_projectedGenerator_of_isMCA (LC : LinearCode ι F) [Nonempty S] (G : Generator S ℓ F)
lemma pseudoinverseGen [DecidableEq ℓ'] [Nonempty S] (G : Generator S ℓ F) (ε_mca : I → ℝ)
lemma tensor_of_MCA_is_MCA [Nonempty S] {S' : Type} [Fintype S'] [Nonempty S'] (LC : LinearCode ι F)
lemma tensor_of_MCA_is_MCA_tight [Nonempty S] {S' : Type} [Fintype S'] [Nonempty S']
noncomputable def zeroExtend (κ : Set ℓ) (U : κ → (ι → F)) : ℓ → (ι → F)

ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean (15)

@[simp] lemma exponentFinsupp_apply {s : ℕ} {d : Fin s → ℕ}
def tensor_of_univ {s : ℕ} (d : Fin s → ℕ) :
lemma coeffMatrix_hasLeftPseudoInverse {s : ℕ} {ℓ : Type} [Fintype ℓ] [DecidableEq ℓ]
lemma exists_exponentFinsupp_eq {s : ℕ} {d : Fin s → ℕ} {mo : Fin s →₀ ℕ} (h : ∀ i, mo i ≤ d i) :
lemma exponentFinsupp_injective {s : ℕ} {d : Fin s → ℕ} :
lemma generatorByRightMul_coeffMatrix {s : ℕ} {ℓ : Type} [Fintype ℓ]
lemma polynomial_gen_MCA_RScode [Fintype F] (n m : ℕ) (hm : 3 ≤ m) {ℓ : Type} [Fintype ℓ] {s : ℕ}
lemma tensor_of_univ_is_MCA [Fintype F] (LC : LinearCode ι F) (ε : ℕ → I → ℝ)
lemma univarite_powers_MCA [Fintype F] (n d m : ℕ) (hm : 3 ≤ m) :
noncomputable def coeffMatrix {s : ℕ} {ℓ : Type} [Fintype ℓ] (P : ℓ → MvPolynomial (Fin s) F)
noncomputable def deg_max {s : ℕ} {ℓ : Type} [Fintype ℓ] (P : ℓ → MvPolynomial (Fin s) F) :
noncomputable def exponentFinsupp {s : ℕ} {d : Fin s → ℕ} (e : (i : Fin s) → Fin (d i + 1)) :
noncomputable def ε_mca_RS [Fintype F] (n d m : ℕ) : I → ℝ
noncomputable def ξ [DecidableEq F] (LC : LinearCode ι F) (d m : ℕ) (η : ℝ) :
theorem polynomial_gen_MCA [DecidableEq F] {ℓ : Type} [Fintype ℓ] (LC : LinearCode ι F) (d : ℕ)

ArkLib/Data/Probability/Instances.lean (4)

theorem Pr_exists_le {α ι : Type} [Fintype ι] (D : PMF α) (f : ι → α → Prop) :
theorem Pr_or_le {α : Type} (D : PMF α) (f g : α → Prop) :
theorem Pr_seq_le_of_forall_le {α β : Type} (Da : PMF α) (Db : PMF β) (Q : α → β → Prop)
theorem prob_uniform_eq_ofReal {F : Type} [Fintype F] [Nonempty F]

✏️ Affected: 3 declaration(s) (line number changed)

def projectedCode [Fintype ι] (C : Set (ι → F)) (T : Finset ι) : Set (T → F) in ArkLib/Data/CodingTheory/Basic/LinearCode.lean moved from L267 to L265
def projectedWord [Fintype ι] (c : ι → F) (T : Finset ι) : T → F in ArkLib/Data/CodingTheory/Basic/LinearCode.lean moved from L260 to L260
def IsMCAGenerator {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (ε_mca : I → ℝ) in ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean moved from L98 to L106

sorry Tracking

❌ Added: 3 `sorry`(s)

ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean (1)

lemma tensor_of_MCA_is_MCA_tight [Nonempty S] {S' : Type} [Fintype S'] [Nonempty S'] (L240)

ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean (2)

lemma univarite_powers_MCA [Fintype F] (n d m : ℕ) (hm : 3 ≤ m) : (L101)
theorem polynomial_gen_MCA [DecidableEq F] {ℓ : Type} [Fintype ℓ] (LC : LinearCode ι F) (d : ℕ) (L70)

📋 **Additional Analysis**

The diff restructures the directory ArkLib/Data/CodingTheory/ProximityGap/ into ArkLib/Data/CodingTheory/ProximityGenerator/, re-exports files, adds AffineGenerator.lean, PolynomialGenerator.lean, updates MCAGenerator.lean and Basic.lean, adds/modifies several lemmas and definitions in existing modules, updates documentation files, and adds probabilistic lemmas. The diff also changes the type of ε_mca from I → I to I → ℝ in several places, adjusts projectedWord and projectedCode to require [Fintype ι], adds a new projectedCode_submod definition, and adjusts IsMCA and IsMCAGenerator accordingly. The doc refs (e.g., docs/kb/concepts/reed-solomon-proximity.md) update paths from ProximityGap to ProximityGenerator. The diff adds AffineGenerator.lean, PolynomialGenerator.lean, and updates Prelims.lean with affineComb, linComb, affineComb_line. The diff adds prob_uniform_eq_ofReal, Pr_or_le, Pr_exists_le, Pr_seq_le_of_forall_le to Instances.lean. The diff adds UnivariatePowers generator, AffineLineGenerator, AffineSpaceGenerator, IsPolynomialGeneratorOfFull, vecMul_tensorGenerator_explicit, isMCAGenerator_reindex, tensor_of_MCA_is_MCA, tensor_of_MCA_is_MCA_tight (sorry). The diff includes a new PolynomialGenerator.lean with deg_max, ξ, polynomial_gen_MCA (sorry), ε_mca_RS, univarite_powers_MCA (sorry), tensor_of_univ, tensor_of_univ_is_MCA, generatorByRightMul_coeffMatrix, coeffMatrix_hasLeftPseudoInverse, polynomial_gen_MCA_RScode (sorry). The diff adjusts poly_gen_is_zero_evading in Basic.lean (formerly ProximityGenerators.lean) and adds error_in_unit_interval, minSeedCard, minSeedCard_pos, minSeedCard_le. The diff modifies ArkLib.lean to import new modules. The diff adds a projectedCode_submod definition in LinearCode.lean. The diff changes IsMCAGenerator error type from I → I to I → ℝ. The diff includes documentation updates in docs/kb/concepts/reed-solomon-proximity.md, docs/kb/papers/BCGM25.md, docs/kb/papers/Jo26.md. The diff includes changes in Prelims.lean: adds affineComb, linComb, affineComb_line. The diff includes changes in Instances.lean: adds prob_uniform_eq_ofReal, Pr_or_le, Pr_exists_le, Pr_seq_le_of_forall_le. The diff removes ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean and ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean, moves their content to ProximityGenerator/ with modifications. The diff updates ArkLib.lean to import from ProximityGenerator instead of ProximityGap. The diff changes H variable in TensorGenerator_Explicit definition? No. The diff changes comments/documentation in Basic.lean. The diff adds -- for TensorGenerator doc? No. The diff adds open Submodule in LinearCode.lean. The diff adds hasSplit and hlin in affineComb_line. The diff adds hcard and hln0 and hsp0 in AffineLine_MCA_AffineSpaceMCA. The diff adds exists_succ_not_mem, projectedQuotient, proj_lincomb_ker_card_le, exists_avg_le, exists_dir_line_ge, exists_line_bound in AffineGenerator.lean. The diff modifies IsPolynomialGeneratorOf comment. The diff adds IsPolynomialGeneratorOfFull definition. The diff adds vecMul_tensorGenerator_explicit. The diff adds tensorProductPiFunEquiv doc? No. The diff adds UnivariatePowers. The diff adds exponentFinsupp, exponentFinsupp_apply, exponentFinsupp_injective, exists_exponentFinsupp_eq, coeffMatrix, generatorByRightMul_coeffMatrix, coeffMatrix_hasLeftPseudoInverse. The diff modifies poly_gen_is_zero_evading proof. The diff adds error_in_unit_interval, minSeedCard, minSeedCard_pos, minSeedCard_le in Basic.lean. The diff adds exists_succ_not_mem, projectedQuotient, proj_lincomb_ker_card_le, exists_avg_le, exists_dir_line_ge, exists_line_bound in AffineGenerator.lean. The diff adds tensor_of_MCA_is_MCA, tensor_of_MCA_is_MCA_tight (sorry), isMCAGenerator_reindex in MCAGenerator.lean. The diff adds polynomial_gen_MCA (sorry), tensor_of_univ_is_MCA, polynomial_gen_MCA_RScode in PolynomialGenerator.lean. The diff adds prob_uniform_eq_ofReal, Pr_or_le, Pr_exists_le, Pr_seq_le_of_forall_le in Instances.lean. The diff adds affineComb, linComb, affineComb_line in Prelims.lean.

📄 **Per-File Summaries**

ArkLib.lean: The diff reorganizes the module hierarchy for proximity generators by adding imports for four new ArkLib.Data.CodingTheory.ProximityGenerator submodules (AffineGenerator, Basic, MCAGenerator, PolynomialGenerator) and removing the two previous ArkLib.Data.CodingTheory.ProximityGap.MCAGenerator and ArkLib.Data.CodingTheory.ProximityGap.ProximityGenerators imports. This migrates the proximity generator definitions from the ProximityGap namespace into a dedicated ProximityGenerator namespace. Neither the old nor the new code introduces any sorry or admit.
ArkLib/Data/CodingTheory/Basic/LinearCode.lean: Added a [Fintype ι] constraint to both projectedWord and projectedCode, ensuring the indexing type is finite for the restriction. Defined projectedCode_submod, a new Submodule F (T → F) whose carrier is the projected code LC.carrier |[T]; the new field proofs (zero_mem', add_mem', smul_mem') establish that the projected code of a linear code is itself an F-submodule. A corresponding open Submodule was also added.
ArkLib/Data/CodingTheory/Prelims.lean: The diff adds two new abbreviations and a lemma to the Affine namespace in ArkLib/Data/CodingTheory/Prelims.lean. The abbreviation affineComb defines the affine combination of codewords U at seed x as Matrix.vecMul (Fin.cons 1 x) U (i.e., U 0 + ∑ i, x i • U (i+1)). The abbreviation linComb defines the linear combination ∑ i, l i • U (i+1) of the direction codewords. The lemma affineComb_line then proves the identity affineComb U (v + t • lam) = affineComb U v + t • (linComb U lam), establishing that the affine combination behaves linearly along a line in seed space.
ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean: This file was deleted. It previously defined the generators generatorByRightMul (right multiplication by a matrix) and projectedGenerator (projection to a subset of coordinates), along with auxiliary definitions matrixMulCodewords and zeroExtend. It contained the lemmas pseudoinverseGen (Lemma 4.1 of BCGM25: right multiplication by a matrix with a left pseudoinverse preserves the MCA property) and generatorSubset (Corollary 4.2 of BCGM25: projection to a subset preserves the MCA property), as well as the supporting lemma isMCA_projectedGenerator_of_isMCA. The deletion removes these results from the codebase; they may have been moved to another location or are no longer needed.
ArkLib/Data/CodingTheory/ProximityGenerator/AffineGenerator.lean: This new file AffineGenerator.lean imports MCAGenerator, Basic, and probability/field theory dependencies and proves Lemma 7.1 from [BCGM25]: mutual correlated agreement (MCA) for the affine line generator implies MCA for the affine space generator. It defines the namespace AffineMCALemmas with the supporting lemmas line_vecMul, exists_succ_not_mem, proj_lincomb_ker_card_le, exists_avg_le, exists_dir_line_ge, and exists_line_bound. The AffineMCAMain namespace contains the main theorem AffineLine_MCA_AffineSpaceMCA, which states that if AffineLineGenerator is an MCA generator with error ε_mca, then AffineSpaceGenerator is an MCA generator with error (1 - 1/|F|)⁻¹ • ε_mca. No sorry or admit are present.
ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean: The file was renamed from ProximityGenerators.lean to Basic.lean under ProximityGenerator. New generator definitions AffineLineGenerator, AffineSpaceGenerator, and UnivariatePowers were added, and a new definition IsPolynomialGeneratorOfFull was introduced as a variant of IsPolynomialGeneratorOf over the whole field. The IsMCA predicate now uses projectedCode_submod instead of projectedCode, and IsMCAGenerator's error parameter type changed from I \u2192 I to I \u2192 \u211d. A lemma vecMul_tensorGenerator_explicit was added, and the proof of poly_gen_is_zero_evading was refactored using convert and any_goals. Additionally, minor documentation fixes (e.g., s replaced \u2113 in IsPolynomialGeneratorOf's docstring, minSeedCard docstring typo corrected) and a new lemma error_in_unit_interval were added. No sorry or admit were introduced.
ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean: This new file defines several transformations on MCA generators (right multiplication by a matrix via generatorByRightMul, projection to a subset of coordinates via projectedGenerator, and tensor product explicitly as TensorGenerator_Explicit) and proves that these transformations preserve the MCA property, formalizing Lemma 4.1 (pseudoinverseGen), Corollary 4.2 (generatorSubset), and Lemma 4.4 (tensor_of_MCA_is_MCA) from [BCGM25]. It also introduces the definitions matrixMulCodewords and zeroExtend used in the proofs, and the lemma isMCAGenerator_reindex for invariance under bijective relabellings. A tighter version of the tensor lemma, tensor_of_MCA_is_MCA_tight, is marked with a sorry pending a planned generalization of IsMCAGenerator to module alphabets.
ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean: This new file (286 lines) introduces definitions and proofs for the Mutual Correlated Agreement (MCA) property of polynomial generators in coding theory. It defines deg_max (maximum degree per variable across a collection of polynomials) and ξ (MCA error for univariate powers, Definition 8.1) and states Theorem 8.2 (polynomial_gen_MCA) establishing MCA for polynomial generators — though the proof is sorry-ed. In the RSCode namespace, it defines ε_mca_RS (specific error function for Reed–Solomon codes, Definition 9.1) and states Lemma 9.3 (univarite_powers_MCA) — also sorry-ed — asserting that univariate powers generators have MCA for Reed–Solomon codes. The file then provides the tensor_of_univ generator (tensor product of univariate powers) and proves tensor_of_univ_is_MCA, showing that tensor products preserve MCA via Lemma 4.4. Two lemmas (generatorByRightMul_coeffMatrix, coeffMatrix_hasLeftPseudoInverse) relate an arbitrary polynomial generator G to the tensor generator via a coefficient matrix and establish that the coefficient matrix has a left pseudo-inverse under linear independence. Finally, Lemma polynomial_gen_MCA_RScode (Theorem 9.2) is proven, using the above results to conclude that any polynomial generator G has MCA for a Reed–Solomon code with error ∑ ε_mca_RS, conditional on the (still sorried) univariate lemma. The file adds the PolynomialGenIsMCA and RSCode namespaces and imports relevant coding theory and mathlib modules.
ArkLib/Data/Probability/Instances.lean: The file adds author Katerina Hristova and moves Real into the existing open block. A new theorem prob_uniform_eq_ofReal (in a dedicated section) expresses the probability of a property under a uniform distribution as ENNReal.ofReal of the ratio |{x: P x}| / |F|, bridging ℝ-valued goals. Three new theorems are appended: Pr_or_le (binary union bound), Pr_exists_le (finite union bound over a Fintype index), and Pr_seq_le_of_forall_le (marginal bound for sequential sampling, stating that if for every b the probability Pr_{a←Da}[Q a b] ≤ c, then the same bound holds for the joint sample Pr_{b←Db; a←Da}[Q a b]).
docs/kb/concepts/reed-solomon-proximity.md: Updated two internal hyperlinks in the documentation file to reflect that the ArkLib modules ProximityGap/ProximityGenerators.lean and ProximityGap/MCAGenerator.lean have been relocated to the ProximityGenerator directory (renamed to ProximityGenerator/Basic.lean and ProximityGenerator/MCAGenerator.lean, respectively). This ensures that the references remain valid after a library reorganization.
docs/kb/papers/BCGM25.md: The file moves two module references from ProximityGap/ to ProximityGenerator/, updating all paths and link texts accordingly (ProximityGenerators.lean → Basic.lean, MCAGenerator.lean unchanged), and renames the subdirectory in two listing sections to reflect the new module structure.
docs/kb/papers/Jo26.md: Updated docs/kb/papers/Jo26.md to correct the file paths for two related modules: ArkLib/Data/CodingTheory/ProximityGenerators.lean was renamed to ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean, and ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean was renamed to ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean. This change ensures the documentation references the correct file locations after a project-wide reorganization.

Last updated: 2026-07-21 15:55 UTC.

github-actions · 2026-07-06T18:31:39Z

🤖 AI Review

Overall Summary:
An error occurred while synthesizing the summary: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

Errors during review:

Agent B failed for ArkLib.lean
Agent B failed for ArkLib/Data/CodingTheory/Basic/LinearCode.lean
Agent B failed for ArkLib/Data/CodingTheory/Prelims.lean
Agent B failed for ArkLib/Data/CodingTheory/ProximityGenerator/AffineGenerator.lean
Agent B failed for ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean
Agent B failed for ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean
Agent B failed for ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean
Agent B failed for ArkLib/Data/Probability/Instances.lean

🔍 **Mechanical Pre-Check Results**

Escape hatches introduced in this PR (triggers hard verdict rule):

sorry introduced in ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean: sorry
sorry introduced in ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean: IsMCAGenerator G ε (ReedSolomon.code D k) := by sorry

Pre-existing escape hatches in touched files (context only, does not affect verdict):

sorry in ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean line 49: sorry
sorry in ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean line 64: IsMCAGenerator G ε (ReedSolomon.code D k) := by sorry

🔗 **Cross-File Analysis**

Cross-file analysis failed: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `ArkLib.lean`**

An error occurred while analyzing ArkLib.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `ArkLib/Data/CodingTheory/Basic/LinearCode.lean`**

An error occurred while analyzing ArkLib/Data/CodingTheory/Basic/LinearCode.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `ArkLib/Data/CodingTheory/Prelims.lean`**

An error occurred while analyzing ArkLib/Data/CodingTheory/Prelims.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `ArkLib/Data/CodingTheory/ProximityGenerator/AffineGenerator.lean`**

An error occurred while analyzing ArkLib/Data/CodingTheory/ProximityGenerator/AffineGenerator.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean`**

An error occurred while analyzing ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean`**

An error occurred while analyzing ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean`**

An error occurred while analyzing ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

📄 **Review for `ArkLib/Data/Probability/Instances.lean`**

An error occurred while analyzing ArkLib/Data/Probability/Instances.lean: 400 INVALID_ARGUMENT. {'error': {'code': 400, 'message': 'API key not valid. Please pass a valid API key.', 'status': 'INVALID_ARGUMENT', 'details': [{'@type': 'type.googleapis.com/google.rpc.ErrorInfo', 'reason': 'API_KEY_INVALID', 'domain': 'googleapis.com', 'metadata': {'service': 'generativelanguage.googleapis.com'}}, {'@type': 'type.googleapis.com/google.rpc.LocalizedMessage', 'locale': 'en-US', 'message': 'API key not valid. Please pass a valid API key.'}]}}

github-actions · 2026-07-26T19:18:05Z

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Polynomial Generators have MCA for RSCodes

sorry delta: +3 (3 added) — proof obligations increased

This pull request formalizes the MCA (Mutual Correlated Agreement) error analysis for polynomial generators, establishing Theorems 8.2 and 9.2 from [BCGM25] (MDS codes and Reed–Solomon codes). It also reorganizes the proximity generator module hierarchy from a flat ProximityGap directory into a granular ProximityGenerator subdirectory (with Basic, AffineGenerator, MCAGenerator, PolynomialGenerator), refactors existing definitions, and adds supporting lemmas across several files.

Mathematical Formalization

Definition 8.1 (MCA error for univariate powers) (ξ): Added in PolynomialGenerator.lean.
Definition 9.1 (RS-specific error) (ε_mca_RS): Added in PolynomialGenerator.lean.
Theorem 8.2 (polynomial_gen_MCA) [BCGM25]: Statement and full proof for generators restricted to subsets of the field. Formalized via UnivariatePowersOn, tensorGeneratorPiUnivariateOn, and polynomial_gen_MCA in PolynomialGenerator.lean.
Theorem 9.2 (polynomial_gen_MCA_RScode) [BCGM25]: Statement and proof assuming Lemma 9.3. The proof uses tensorGeneratorPiUnivariate.isMCAGenerator (new) and tensorGeneratorPi.isMCAGenerator (iterated Lemma 4.4). The proof explicitly constructs the matrix A that appears in the paper's proof.
Lemma 9.3 (univariate_powers_MCA): LEFT AS sorry in PolynomialGenerator.lean. All uses of Theorem 9.2 assume this lemma.
Theorem 6.1 (isMCAGenerator_of_isMDSGenerator) [BCGM25]: LEFT AS sorry in MCAGenerator.lean. Statement only; proof not yet provided.
MCA error function for MDS codes (ε_MCA_MDS): Defined in MCAGenerator.lean.
Lemma 7.1 (AffineLine_MCA_AffineSpaceMCA): Fully proved in AffineGenerator.lean (affine line MCA ⇒ affine space MCA with scaled error), with auxiliary lemmas (line_vecMul, exists_succ_not_mem, proj_lincomb_ker_card_le, exists_avg_le, exists_dir_line_ge, exists_line_bound).
Tensor product lemmas: tensor_of_MCA_is_MCA (proved in MCAGenerator.lean; error ε_mca + |ℓ| • ε_mca'). The tight version tensor_of_MCA_is_MCA_tight (error ε_mca + ε_mca') is LEFT AS sorry. A more general result than the paper's version for Reed–Solomon codes is proved: tensor_of_univ_is_MCA holds for any univariate generator.
coeffMatrix and generatorByRightMul_coeffMatrix: Defined in PolynomialGenerator.lean. coeffMatrix_hasLeftPseudoInverse connects polynomial generators to the tensor generator via right multiplication by a left-pseudoinvertible matrix.
Affine generator definition: AffineLineGenerator and AffineSpaceGenerator added in Basic.lean.
UnivariatePowers generator: Added in Basic.lean (maps x → (1,x,x^2,…,x^d)).
IsPolynomialGeneratorOfFull: Added in Basic.lean (special case where each seed component is the whole field).
vecMul_tensorGenerator_explicit: Lemma expressing vector–matrix multiplication of the explicit tensor generator in factorized form (Basic.lean).
Helper lemmas: affineComb, linComb, and lemma affineComb_line added in Prelims.lean.
Projection / submodule code: projectedWord and projectedCode now require [Fintype ι]; projectedCode now calls projectedWord explicitly instead of using removed notation C|[T]. New definition projectedCode_submod (LinearCode.lean). IsMCA now references projectedCode_submod (Basic.lean).
isMCAGenerator_reindex: Invariance under bijective relabelings (MCAGenerator.lean).
Generator-by-right-multiplication (generatorByRightMul) and projectedGenerator (MCAGenerator.lean).
Probability theorems: prob_uniform_eq_ofReal, Pr_or_le (binary union bound), Pr_exists_le (generalized union bound for finite index sets), Pr_seq_le_of_forall_le (marginal bound for sequential sampling) added in Instances.lean.

Refactoring / Infrastructure

Module reorganization: The flat ProximityGap/ directory is replaced by ProximityGenerator/ with four files: Basic, AffineGenerator, MCAGenerator, PolynomialGenerator. The main ArkLib.lean import list updated accordingly. The docs/kb/concepts/reed-solomon-proximity.md, docs/kb/papers/BCGM25.md, and docs/kb/papers/Jo26.md files update all references to reflect the new paths. A new touchpoint ArkLib/ProofSystem/Whir/MutualCorrAgreement.lean added to BCGM25.md.
Basic.lean refactor: The original ProximityGap/ProximityGenerators.lean is moved to ProximityGenerator/Basic.lean. The ε_mca parameter type changed from I → I to I → ℝ. The proof of poly_gen_is_zero_evading refactored using convert and any_goals. Several docstrings improved.

sorry / admit placeholders (to be completed)

univariate_powers_MCA (Lemma 9.3) in PolynomialGenerator.lean: sorry — blocks a self-contained proof of Theorem 9.2.
isMCAGenerator_of_isMDSGenerator (Theorem 6.1) in MCAGenerator.lean: sorry — statement only.
tensor_of_MCA_is_MCA_tight in MCAGenerator.lean: sorry — tight error bound not yet proved.

No other sorries or admits are present anywhere in the changed files.

Statistics

Metric	Count
📝 Files Changed	12
✅ Lines Added	1268
❌ Lines Removed	171

Lean Declarations

✏️ Removed: 7 declaration(s)

ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean (7)

def generatorByRightMul (G : Generator S ℓ F) (A : Matrix ℓ ℓ' F) : Generator S ℓ' F
def matrixMulCodewords (A : Matrix ℓ ℓ' F) (U : ℓ' → (ι → F)) : ℓ → (ι → F)
def projectedGenerator (G : Generator S ℓ F) (κ : Set ℓ) : Generator S κ F
lemma generatorSubset [Nonempty S] (G : Generator S ℓ F) (ε_mca : I → I) (LC : LinearCode ι F)
lemma isMCA_projectedGenerator_of_isMCA (LC : LinearCode ι F) [Nonempty S] (G : Generator S ℓ F)
lemma pseudoinverseGen [DecidableEq ℓ'] [Nonempty S] (G : Generator S ℓ F) (ε_mca : I → I)
noncomputable def zeroExtend (κ : Set ℓ) (U : κ → (ι → F)) : ℓ → (ι → F)

✏️ Added: 57 declaration(s)

ArkLib/Data/CodingTheory/Basic/LinearCode.lean (1)

def projectedCode_submod

ArkLib/Data/CodingTheory/Prelims.lean (3)

abbrev affineComb {s : ℕ} (U : Fin (s + 1) → (ι → F)) (x : Fin s → F) : ι → F
abbrev linComb {s : ℕ} (U : Fin (s + 1) → (ι → F)) (l : Fin s → F) : ι → F
lemma affineComb_line {s : ℕ} (U : Fin (s + 1) → (ι → F)) (v lam : Fin s → F) (t : F) :

ArkLib/Data/CodingTheory/ProximityGenerator/AffineGenerator.lean (8)

abbrev projectedQuotient [Fintype ι] (LC : LinearCode ι F) (T : Finset ι) : Type
lemma exists_avg_le [Fintype F] {s : ℕ} (hs : 1 ≤ s) (f : (Fin s → F) → ℕ) (m : ℕ)
lemma exists_dir_line_ge [Fintype F] [Nonempty F] {s : ℕ}
lemma exists_line_bound [Fintype F] [Fintype ι] {s : ℕ} (hs : 1 ≤ s)
lemma exists_succ_not_mem [Fintype ι] {s : ℕ} (LC : LinearCode ι F) (T : Finset ι)
lemma line_vecMul (W : Fin 2 → (ι → F)) (t : F) :
lemma proj_lincomb_ker_card_le [Fintype F] [Fintype ι] {s : ℕ}
theorem AffineLine_MCA_AffineSpaceMCA {ℓ : ℕ} (hℓ : ℓ ≥ 2) (ε_mca : I → ℝ) (LC : LinearCode ι F)

ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean (5)

abbrev AffineLineGenerator (F : Type) [Field F] : Generator F (Fin 2) F
abbrev AffineSpaceGenerator (F : Type) [Field F] (ℓ : ℕ) : Generator (Fin ℓ → F) (Fin (ℓ + 1)) F
def IsPolynomialGeneratorOfFull {s : ℕ} (G : Generator (Fin s → F) ℓ F)
def UnivariatePowers (d : ℕ) : Generator F (Fin (d + 1)) F
lemma vecMul_tensorGenerator_explicit {ℓ' : Type} [Fintype ℓ'] {S S' : Type}

ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean (12)

def generatorByRightMul (G : Generator S ℓ F) (A : Matrix ℓ ℓ' F) : Generator S ℓ' F
def matrixMulCodewords (A : Matrix ℓ ℓ' F) (U : ℓ' → (ι → F)) : ℓ → (ι → F)
def projectedGenerator (G : Generator S ℓ F) (κ : Set ℓ) : Generator S κ F
lemma generatorSubset [Nonempty S] (G : Generator S ℓ F) (ε_mca : I → ℝ) (LC : LinearCode ι F)
lemma isMCAGenerator_reindex {S' : Type} [Fintype S'] [Nonempty S'] [Nonempty S]
lemma isMCA_projectedGenerator_of_isMCA (LC : LinearCode ι F) [Nonempty S] (G : Generator S ℓ F)
lemma pseudoinverseGen [DecidableEq ℓ'] [Nonempty S] (G : Generator S ℓ F) (ε_mca : I → ℝ)
lemma tensor_of_MCA_is_MCA [Nonempty S] {S' : Type} [Fintype S'] [Nonempty S'] (LC : LinearCode ι F)
lemma tensor_of_MCA_is_MCA_tight [Nonempty S] {S' : Type} [Fintype S'] [Nonempty S']
noncomputable def zeroExtend (κ : Set ℓ) (U : κ → (ι → F)) : ℓ → (ι → F)
noncomputable def ε_MCA_MDS [DecidableEq F] [Nonempty ι] (LC : LinearCode ι F) (ℓ s : ℕ) (η : ℝ) :
theorem isMCAGenerator_of_isMDSGenerator {S : Type} [Nonempty S] [Fintype S] [DecidableEq F]

ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean (24)

def UnivariatePowersOn (s : Set F) (d : ℕ) : Generator s (Fin (d + 1)) F
def tensorGeneratorPi {s : ℕ} {α : Fin s → Type} {ℓ : Fin s → Type}
def tensorGeneratorPiUnivariate {s : ℕ} (d : Fin s → ℕ) :
def tensorGeneratorPiUnivariateOn {s : ℕ} (S : Fin s → Set F) (d : Fin s → ℕ) :
lemma UnivariatePowersOn.code_eq_reedSolomon (s : Set F) [Fintype s] [Nonempty s] (d : ℕ) :
lemma UnivariatePowersOn.isMCAGenerator {ι : Type} [Fintype ι] [Nonempty ι] [DecidableEq F]
lemma UnivariatePowersOn.isMDSGenerator [DecidableEq F] (s : Set F) [Fintype s] [Nonempty s]
lemma coeffMatrix_hasLeftPseudoInverse {s : ℕ} {ℓ : Type} [Fintype ℓ] [DecidableEq ℓ]
lemma exists_exponentFinsupp_eq {s : ℕ} {d : Fin s → ℕ} {mo : Fin s →₀ ℕ} (h : ∀ i, mo i ≤ d i) :
lemma exponentFinsupp_injective {s : ℕ} {d : Fin s → ℕ} :
lemma generatorByRightMul_coeffMatrix {s : ℕ} {ℓ : Type} [Fintype ℓ]
lemma generatorByRightMul_coeffMatrix_sub {s : ℕ} {ℓ : Type} [Fintype ℓ]
lemma polynomial_gen_MCA_RScode [Fintype F] (n m : ℕ) (hm : 3 ≤ m) {ℓ : Type} [Fintype ℓ] {s : ℕ}
lemma tensorGeneratorPiUnivariateOn_isMCAGenerator {ι : Type} [Fintype ι] [Nonempty ι]
lemma tensorGeneratorPiUnivariate_isMCAGenerator [Fintype F] (LC : LinearCode ι F)
lemma tensorGeneratorPi_isMCAGenerator (LC : LinearCode ι F) :
lemma univariate_powers_MCA [Fintype F] (n d m : ℕ) (hm : 3 ≤ m) :
lemma ε_MCA_MDS_eq_ξ [DecidableEq F] (LC : LinearCode ι F) (d m : ℕ) (η : ℝ) :
noncomputable def coeffMatrix {s : ℕ} {ℓ : Type} [Fintype ℓ] (P : ℓ → MvPolynomial (Fin s) F)
noncomputable def deg_max {s : ℕ} {ℓ : Type} [Fintype ℓ] (P : ℓ → MvPolynomial (Fin s) F) :
noncomputable def exponentFinsupp {s : ℕ} {d : Fin s → ℕ} (e : (i : Fin s) → Fin (d i + 1)) :
noncomputable def ε_mca_RS [Fintype F] (n d m : ℕ) : I → ℝ
noncomputable def ξ [DecidableEq F] (LC : LinearCode ι F) (d m : ℕ) (η : ℝ) :
theorem polynomial_gen_MCA {ι : Type} [Fintype ι] [Nonempty ι] [DecidableEq F]

ArkLib/Data/Probability/Instances.lean (4)

theorem Pr_exists_le {α ι : Type} [Fintype ι] (D : PMF α) (f : ι → α → Prop) :
theorem Pr_or_le {α : Type} (D : PMF α) (f g : α → Prop) :
theorem Pr_seq_le_of_forall_le {α β : Type} (Da : PMF α) (Db : PMF β) (Q : α → β → Prop)
theorem prob_uniform_eq_ofReal {F : Type} [Fintype F] [Nonempty F]

✏️ Affected: 3 declaration(s) (line number changed)

def projectedCode [Fintype ι] (C : Set (ι → F)) (T : Finset ι) : Set (T → F) in ArkLib/Data/CodingTheory/Basic/LinearCode.lean moved from L267 to L265
def projectedWord [Fintype ι] (c : ι → F) (T : Finset ι) : T → F in ArkLib/Data/CodingTheory/Basic/LinearCode.lean moved from L260 to L260
def IsMCAGenerator {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (ε_mca : I → ℝ) in ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean moved from L98 to L106

sorry Tracking

❌ Added: 3 `sorry`(s)

ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean (2)

lemma tensor_of_MCA_is_MCA_tight [Nonempty S] {S' : Type} [Fintype S'] [Nonempty S'] (L223)
theorem isMCAGenerator_of_isMDSGenerator {S : Type} [Nonempty S] [Fintype S] [DecidableEq F] (L252)

ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean (1)

lemma univariate_powers_MCA [Fintype F] (n d m : ℕ) (hm : 3 ≤ m) : (L170)

📋 **Additional Analysis**

The diff contains a substantial refactor that renames the directory ProximityGap to ProximityGenerator, moves/rewrites MCAGenerator.lean and ProximityGenerators.lean into that new directory, adds a new AffineGenerator.lean, adds a LinearCode submodule projectedCode_submod, relaxes projectedWord/projectedCode to require [Fintype ι], adjusts IsMCAGenerator to take ε_mca : I → ℝ, adds the PolynomialGenerator.lean file with Theorem 8.2 and a major portion of Section 9 of BCGM25, and adds UnivariatePowers/AffineLineGenerator/AffineSpaceGenerator generators plus associated MCA lemmas. Doc pages (.md files) are updated to reflect the new import paths.

📄 **Per-File Summaries**

ArkLib.lean: The import list in ArkLib.lean was updated to replace two modules from the ProximityGap directory with four modules from a new ProximityGenerator directory. Specifically, ArkLib.Data.CodingTheory.ProximityGap.MCAGenerator and ProximityGap.ProximityGenerators were removed, and ArkLib.Data.CodingTheory.ProximityGenerator.AffineGenerator, ProximityGenerator.Basic, ProximityGenerator.MCAGenerator, and ProximityGenerator.PolynomialGenerator were added. This reflects a restructuring of the proximity generator definitions into a more granular module hierarchy, with separate files for affine, polynomial, and basic generators, as well as an updated MCAGenerator.
ArkLib/Data/CodingTheory/Basic/LinearCode.lean: The definitions projectedWord and projectedCode now require a [Fintype ι] typeclass argument, and their associated notation macros (c|[T] and C|[T]) have been removed; projectedCode now calls projectedWord explicitly instead of using the removed notation. A new definition projectedCode_submod is added, which constructs a Submodule F (T → F) whose carrier is projectedCode (LC.carrier) T, with proofs of zero_mem', add_mem', and smul_mem' (using Submodule.add_mem_iff_right and Submodule.smul_mem). No sorry or admit appear in the diff.
ArkLib/Data/CodingTheory/Prelims.lean: Added two abbrevs, affineComb and linComb, defining affine and linear combinations of Fin (s+1) → (ι → F) under a seed x and coefficients l, respectively. Added lemma affineComb_line (proved using Matrix.add_vecMul and Matrix.smul_vecMul) which states affineComb U (v + t • lam) = affineComb U v + t • (linComb U lam). The lemma uses an omit clause to drop Fintype assumptions on ι and F. A blank line was also inserted for formatting.
ArkLib/Data/CodingTheory/ProximityGenerator/AffineGenerator.lean: This new file introduces supporting lemmas and a main theorem for Lemma 7.1 of [BCGM25], which states that if the affine line generator AffineLineGenerator has mutual correlated agreement (MCA) error ε_mca for a linear code LC, then the affine space generator AffineSpaceGenerator has MCA error scaled by (1-1/|F|)⁻¹. Key additions include: line_vecMul, exists_succ_not_mem, proj_lincomb_ker_card_le, exists_avg_le, exists_dir_line_ge, and exists_line_bound lemmas in the AffineMCALemmas namespace, each establishing intermediate combinatorial or linear-algebraic bounds. The main theorem AffineLine_MCA_AffineSpaceMCA in the AffineMCAMain namespace proves the implication, using probabilistic and averaging arguments over finite fields. No sorries or admits appear in the diff.
ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean: The file was renamed from ProximityGap/ProximityGenerators.lean to ProximityGenerator/Basic.lean and received several additions and modifications. Four new definitions were added: IsPolynomialGeneratorOfFull (a special case of polynomial generator where each seed component is the whole field), AffineLineGenerator (maps x to (1,x)), AffineSpaceGenerator (maps a length-ℓ vector to (1,x)), and UnivariatePowers (maps x to the list (1,x,x²,…,x^d)). A new lemma vecMul_tensorGenerator_explicit expresses the vector–matrix multiplication of the explicit tensor generator in factorized form. In existing definitions, IsMCA now references projectedCode_submod instead of projectedCode, and the error parameter ε_mca of IsMCAGenerator was changed from I → I to I → ℝ. The proof of poly_gen_is_zero_evading was refactored to use convert and any_goals. Several docstrings were improved (e.g., correcting the number of subsets in IsPolynomialGeneratorOf, clarifying the minimum-seed-cardinality documentation, and adding a docstring to error_in_unit_interval). No sorry or admit were introduced.
ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean: This file introduces definitions and lemmas for MCA (Mutual Correlated Agreement) generators, formalizing several results from [BCGM25]. It defines generatorByRightMul (right multiplication by a matrix), projectedGenerator (restriction to a coordinate subset), matrixMulCodewords (left multiplication on codewords), and zeroExtend (extension by zeros). Key lemmas include pseudoinverseGen (Lemma 4.1: an MCA generator remains MCA under right multiplication by a left-pseudoinvertible matrix), generatorSubset (Corollary 4.2: projection preserves MCA), isMCAGenerator_reindex (invariance under bijective relabelings), and tensor_of_MCA_is_MCA (tensor product of two MCA generators is MCA with error ε_mca + |ℓ| • ε_mca'). The statement tensor_of_MCA_is_MCA_tight (tensor product with error ε_mca + ε_mca') is present but currently left as sorry. The file also defines ε_MCA_MDS, the MCA error function for MDS codes, and states isMCAGenerator_of_isMDSGenerator (Theorem 6.1), which is also sorryed.
ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean: This new file PolynomialGenerator.lean defines and proves MCA (mutual correlated agreement) properties for polynomial generators, establishing Theorem 8.2 and Theorem 9.2 of [BCGM25]. Key additions include: the MCA error function ξ (Definition 8.1); tensorGeneratorPi and its MCA lemma tensorGeneratorPi_isMCAGenerator (iterated Lemma 4.4); ε_mca_RS (Definition 9.1, the RS-specific error); the sorried lemma univariate_powers_MCA (Lemma 9.3); tensorGeneratorPiUnivariate and its MCA lemma; coeffMatrix, generatorByRightMul_coeffMatrix, and coeffMatrix_hasLeftPseudoInverse connecting polynomial generators to the tensor generator; polynomial_gen_MCA_RScode (Theorem 9.2); and UnivariatePowersOn, tensorGeneratorPiUnivariateOn, and polynomial_gen_MCA (Theorem 8.2) for generators restricted to subsets of the field.
ArkLib/Data/Probability/Instances.lean: Added three new theorems to ArkLib/Data/Probability/Instances.lean. prob_uniform_eq_ofReal provides an ENNReal.ofReal-based expression for uniform probability over a finite type, converting the existing prob_uniform_eq_card_filter_div_card result to the real-number representation. Pr_or_le establishes the binary union bound: the probability of a disjunction of two events is at most the sum of their individual probabilities. Pr_exists_le generalizes this to finite index sets, bounding the probability of ∃ i, f i r by the sum over i of the probabilities of each f i r. Pr_seq_le_of_forall_le proves a marginal bound for sequential sampling: if for every fixed b the marginal probability over a of Q a b is at most c, then the joint probability over the sequential sample (b, a) ← (Db, Da) is also at most c. No sorries or admits are introduced.
docs/kb/concepts/reed-solomon-proximity.md: This documentation change updates the ArkLib import links in the "References" section of the reed-solomon-proximity.md file. The two previously listed files (ProximityGap/ProximityGenerators.lean and ProximityGap/MCAGenerator.lean) have been renamed: the directory ProximityGap is replaced by ProximityGenerator, and the first file is now ProximityGenerator/Basic.lean. These updates keep the documentation's file paths aligned with the actual ArkLib library structure after a reorganization of the proximity generator code.
docs/kb/papers/BCGM25.md: This change updates docs/kb/papers/BCGM25.md to reflect a refactor of the ArkLib codebase: the CodingTheory/ProximityGap/ directory has been renamed to CodingTheory/ProximityGenerator/, so all file links and references in the document are updated accordingly (e.g., ProximityGenerators.lean → ProximityGenerator/Basic.lean, MCAGenerator.lean → ProximityGenerator/MCAGenerator.lean). Additionally, a new touchpoint ArkLib/ProofSystem/Whir/MutualCorrAgreement.lean is added to the 'Main ArkLib Touchpoints' section.
docs/kb/papers/Jo26.md: Updated the documentation file docs/kb/papers/Jo26.md to reflect the renaming of the module path ProximityGap/ProximityGenerators to ProximityGenerator/Basic and ProximityGap/MCAGenerator to ProximityGenerator/MCAGenerator. The references in the YAML front-matter related_modules list and the in-text links were both updated to point to the new module paths. The change aligns the documentation with the refactored directory structure for these coding theory modules and does not alter any conceptual content or theorems.
1 file(s) filtered as noise (lockfiles, generated, or trivial): ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean

Last updated: 2026-07-27 11:24 UTC.

alexanderlhicks · 2026-08-05T18:45:54Z

+
+/-- The restricted univariate powers generator is an MDS generator (its code is Reed–Solomon,
+hence MDS). -/
+lemma UnivariatePowersOn.isMDSGenerator [DecidableEq F] (s : Set F) [Fintype s] [Nonempty s]


quick note that ismDS will require [Inhabited ι] now that #663 has merged, which will allow you to remove (h : d + 1 ≤ Fintype.card ↥s)

alexanderlhicks · 2026-08-05T18:47:15Z

+  · have hℓ : 2 ≤ Fintype.card (Fin (d + 1)) := by rw [Fintype.card_fin]; omega
+    have hdim : LinearCode.dim (fromColGenMat (M_G (UnivariatePowersOn s d)))
+        = Fintype.card (Fin (d + 1)) := by
+      rw [UnivariatePowersOn.code_eq_reedSolomon, ReedSolomon.dim_eq_deg_of_le' h, Fintype.card_fin]


also a note that ReedSolomon.dim_eq_deg_of_le' can be replaced by ReedSolomon.dim_eq_deg_of_le now.

alexanderlhicks · 2026-08-05T18:49:42Z

+
+
+/-- Definition 9.1 MCA error function for Reed-Solomon codes [BCGM25]. -/
+noncomputable def ε_mca_RS [Fintype F] (n d m : ℕ) : I → ℝ :=


n is the block length so it should be constrained to be Fintype.card ι (line 47 above exemplifies this).
Same in other statements below.

alexanderlhicks · 2026-08-05T19:14:40Z

+  let ρ_sqrt := ReedSolomon.sqrtRate k D
+  fun γ =>
+    if γ ≤ 1 - (1 + (1 / (2 * m : ℝ))) * ρ_sqrt then
+      (|Fintype.card F| : ℝ)⁻¹  *  (m + 1 / 2) ^ 7  * (3 * (ρ_sqrt) ^ 3)⁻¹.toReal * d * n ^ 2


careful with this because ρ_sqrt := ReedSolomon.sqrtRate is R >= 0, and lean will allow division by 0 which is implicitely gaurded against in the paper definition. k > 0 should prevent this?

alexanderlhicks · 2026-08-05T19:15:58Z

+  let ρ_sqrt := ReedSolomon.sqrtRate k D
+  fun γ =>
+    if γ ≤ 1 - (1 + (1 / (2 * m : ℝ))) * ρ_sqrt then
+      (|Fintype.card F| : ℝ)⁻¹  *  (m + 1 / 2) ^ 7  * (3 * (ρ_sqrt) ^ 3)⁻¹.toReal * d * n ^ 2


|Fintype.card F| can just be Fintype.card F

alexanderlhicks · 2026-08-05T19:31:54Z

+def projectedWord [Fintype ι] (c : ι → F) (T : Finset ι) : T → F := Set.restrict T c

 /-- Let `C` be a code of length `ι`. For every finite `ι`-subset `T`, we define the projected code
 `C|[T]` as the set of projected codewords `c|[T]`, for `c ∈ C`.


minor docstring change after the notation change in #596

alexanderlhicks · 2026-08-05T19:33:56Z

+/-- A function assinging the maximum degree in the `i`-the variable of the collection of
+polynomials `P`. -/
+noncomputable def deg_max {s : ℕ} {ℓ : Type} [Fintype ℓ] (P : ℓ → MvPolynomial (Fin s) F) :
+    Fin s → ℕ := fun i => Finset.sup Fintype.elems (fun j => (P j).degreeOf i)


finset.uni is seemingly more popular/standard than .elems. I don't really know if it's a big deal, but it keeps the definition in terms of finset only.

alexanderlhicks · 2026-08-05T19:38:30Z

+  apply ENNReal.tsum_le_tsum
+  intro r
+  rw [← mul_add]
+  refine mul_le_mul_of_nonneg_left ?_ zero_le'


linter says use zero_le

alexanderlhicks · 2026-08-05T19:38:41Z

+    _ ≤ ∑' b, Db b * c := by
+        apply ENNReal.tsum_le_tsum
+        intro b
+        exact mul_le_mul_of_nonneg_left (h b) zero_le'


linter says use zero_le

alexanderlhicks · 2026-08-05T19:39:58Z

+The affine line generator `F → F²`, `x ↦ (1, x)`, having MCA error `ε_mca` for `LC` implies that
+the affine space generator `Fˡ → Fˡ⁺¹`, `x ↦ (1, x)`, has MCA for `LC` with error
+`(1 - 1/|F|)⁻¹ • ε_mca`. -/
+theorem AffineLine_MCA_AffineSpaceMCA {ℓ : ℕ} (hℓ : ℓ ≥ 2) (ε_mca : I → ℝ) (LC : LinearCode ι F)


worth merging in main to get rid of ε_mca : I → ℝ now that #596 is merged

katyhr added 30 commits May 4, 2026 13:30

port prelims from pr

d1ed9a1

port basic from pr

084f588

changes from PR

60f9f80

new dependencies

f1011fc

lin combo lemmas

ad2f00e

defs from section 3

0fbc738

ArkLib/Data/CodingTheory/Basic/MDSCode.lean

f3e1433

minor edits

b9bc283

SZ counting form for rmk 320

2d300f2

remove lint errors

924b6c3

one more lint error

9407ee0

tensor gen def

4eb5b04

tensor of gens

347eb35

lemma 4.1 cor 4.2

3aaa220

update dependencies

e23c8e5

broken proof drafts

e1213de

next draft

0e7be75

lemmas from section 4_1

d9ca194

update dependencies

be2b1d6

linear combos in projected codes

d175c68

tensor gens def

ec65ec5

pseudoinverses

1146d2b

monotonicity lemma

57b1fcd

small edits

19d3db2

change S S' to general types

30d14f3

remove monotonicity lemma

fbbc5d8

small changes

3939acc

Merge branch 'main' into Katy/MCAgens

93d65a1

update imports

1c72ed5

merge main

e7e942d

katyhr added 6 commits June 30, 2026 14:24

cleanup

3cf6023

fix linter

6d498c1

another linter error

f340d76

Merge branch 'main' into Katy/AffineGens

c9ea16e

tensor gens lemma weak bound

300730d

refactor + first draft

958b9be

katyhr added 7 commits July 8, 2026 23:25

draft 1

5cfdb01

cleanup of section 9

837b03c

Merge branch 'main' into Katy/RScodeMCA

d521deb

some errors

48c467d

correct links

05b2c65

update with the refactor:

715d232

edit docs

dd934d2

katyhr marked this pull request as ready for review July 21, 2026 11:19

katyhr requested a review from alexanderlhicks July 21, 2026 11:19

katyhr added 3 commits July 21, 2026 16:51

some edits

66a3181

formalisation of theorem 6.1. and proofs of section 8

e72c20c

rename theorem 6.1

37ed6cf

katyhr and others added 3 commits July 26, 2026 20:19

Merge branch 'main' into Katy/RScodeMCA

6dcea6e

minor edits

0c384c8

edit docstrings

e3e8d1e

alexanderlhicks reviewed Aug 5, 2026

View reviewed changes

Navigation Menu

Uh oh!

Polynomial Generators have MCA for RSCodes - #610

Polynomial Generators have MCA for RSCodes#610
katyhr wants to merge 77 commits into
mainfrom
Katy/RScodeMCA

katyhr commented Jul 6, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Jul 6, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Jul 6, 2026

Uh oh!

github-actions Bot commented Jul 26, 2026 •

edited

Loading

Uh oh!

alexanderlhicks Aug 5, 2026

Uh oh!

alexanderlhicks Aug 5, 2026

Uh oh!

alexanderlhicks Aug 5, 2026

Uh oh!

alexanderlhicks Aug 5, 2026

Uh oh!

alexanderlhicks Aug 5, 2026

Uh oh!

alexanderlhicks Aug 5, 2026

Uh oh!

alexanderlhicks Aug 5, 2026

Uh oh!

alexanderlhicks Aug 5, 2026

Uh oh!

alexanderlhicks Aug 5, 2026

Uh oh!

alexanderlhicks Aug 5, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants



		/-- Definition 9.1 MCA error function for Reed-Solomon codes [BCGM25]. -/
		noncomputable def ε_mca_RS [Fintype F] (n d m : ℕ) : I → ℝ :=

Uh oh!

Conversation

katyhr commented Jul 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 PR Summary

Uh oh!

github-actions Bot commented Jul 6, 2026

🤖 AI Review

Uh oh!

github-actions Bot commented Jul 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 PR Summary

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

katyhr commented Jul 6, 2026 •

edited

Loading

github-actions Bot commented Jul 6, 2026 •

edited

Loading

github-actions Bot commented Jul 26, 2026 •

edited

Loading